;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark -*-
;;; File: code-for-numbers2.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2006.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.

(in-package :snark)

;;; SNARK can evaluate numerical expressions as if by table lookup for
;;; procedurally attached relations or functions
;;;
;;; numeric operations are over the rationals or floats, but not mixtures of them
;;;
;;; in SNARK, 2 and 2.0 are unequal and the rational and floating-point
;;; numeric domains are unrelated except for
;;; the $$rationalize and $$float conversion operations
;;; that convert floats to rationals and rationals to floats
;;;
;;; what SNARK "knows" about numbers is limited by this notion of
;;; table lookup; no more general properties are known
;;; like (= (+ x 0) x), (= (* x 0) 0), (exists (x) (< x 0)),
;;; associativity and commutativity of + and *, etc.
;;;
;;; this is intended only to provide simple numeric calculation,
;;; not any symbolic algebra, and be precise about what SNARK
;;; is and is not capable of numerically
;;;
;;; ($$less a b)       is rewritten to true or false depending on the value of (< a b) if a and b are both rational number constants or both floating-point constants
;;; ($$lesseq a b)     is rewritten to true or false depending on the value of (<= a b) if a and b are both rational number constants or both floating-point constants
;;; ($$greater a b)    is rewritten to true or false depending on the value of (> a b) if a and b are both rational number constants or both floating-point constants
;;; ($$greatereq a b)  is rewritten to true or false depending on the value of (>= a b) if a and b are both rational number constants or both floating-point constants
;;;
;;; operations on rationals:
;;; ($$sum a b)        is rewritten to the value of (+ a b) if a and b are rational number constants
;;; ($$product a b)    is rewritten to the value of (* a b) if a and b are rational number constants
;;; ($$difference a b) is rewritten to the value of (- a b) if a and b are rational number constants
;;; ($$quotient a b)   is rewritten to the value of (/ a b) if a and b are rational number constants
;;; ($$ceiling a b)    is rewritten to the value of (ceiling a b) if a and b are rational number constants
;;; ($$floor a b)      is rewritten to the value of (floor a b) if a and b are rational number constants
;;; ($$round a b)      is rewritten to the value of (round a b) if a and b are rational number constants
;;; ($$truncate a b)   is rewritten to the value of (truncate a b) if a and b are rational number constants
;;; ($$uminus a)       is rewritten to the value of (- a) if a is a rational number constant
;;; ($$ceiling a)      is rewritten to the value of (ceiling a) if a is a rational number constant
;;; ($$floor a)        is rewritten to the value of (floor a) if a is a rational number constant
;;; ($$round a)        is rewritten to the value of (round a) if a is a rational number constant
;;; ($$truncate a)     is rewritten to the value of (truncate a) if a is a rational number constant
;;; ($$float a)        is rewritten to the value of (float a) if a is a rational number constant
;;;
;;; operations on floats:
;;; ($$sum_float a b)        is rewritten to the value of (+ a b) if a and b are rational number constants
;;; ($$product_float a b)    is rewritten to the value of (* a b) if a and b are rational number constants
;;; ($$difference_float a b) is rewritten to the value of (- a b) if a and b are rational number constants
;;; ($$quotient_float a b)   is rewritten to the value of (/ a b) if a and b are rational number constants
;;; ($$ceiling_float a b)    is rewritten to the value of (fceiling a b) if a and b are rational number constants
;;; ($$floor_float a b)      is rewritten to the value of (ffloor a b) if a and b are rational number constants
;;; ($$round_float a b)      is rewritten to the value of (fround a b) if a and b are rational number constants
;;; ($$truncate_float a b)   is rewritten to the value of (ftruncate a b) if a and b are rational number constants
;;; ($$uminus_float a)       is rewritten to the value of (- a) if a is a rational number constant
;;; ($$ceiling_float a)      is rewritten to the value of (fceiling a) if a is a rational number constant
;;; ($$floor_float a)        is rewritten to the value of (ffloor a) if a is a rational number constant
;;; ($$round_float a)        is rewritten to the value of (fround a) if a is a rational number constant
;;; ($$truncate_float a)     is rewritten to the value of (ftruncate a) if a is a rational number constant
;;; ($$rationalize a)        is rewritten to the value of (rationalize a) if a is floating-point number constant
;;; 
;;; operations on integers:
;;; ($$sum_integer a b)        is rewritten to the value of (+ a b) if a and b are integer number constants
;;; ($$product_integer a b)    is rewritten to the value of (* a b) if a and b are integer number constants
;;; ($$difference_integer a b) is rewritten to the value of (- a b) if a and b are integer number constants
;;; ($$quotient_integer a b)   is rewritten to the value of (/ a b) if a and b are integer number constants rounded to an integer according to (integer-quotient-rounding-mode?)
;;; ($$ceiling_integer a b)    is rewritten to the value of (ceiling a b) if a and b are integer number constants
;;; ($$floor_integer a b)      is rewritten to the value of (floor a b) if a and b are integer number constants
;;; ($$round_integer a b)      is rewritten to the value of (round a b) if a and b are integer number constants
;;; ($$truncate_integer a b)   is rewritten to the value of (truncate a b) if a and b are integer number constants
;;; ($$uminus_integer a)       is rewritten to the value of (- a) if a is an integer number constant

(declare-snark-option integer-quotient-rounding-mode 'truncate 'truncate)

(defun declare-code-for-numbers2 ()
  (declare-relation-rewriter1 '$$numberp     1 'numberp-atom-rewriter)
  (declare-relation-rewriter1 '$$realp       1 'realp-atom-rewriter)
  (declare-relation-rewriter1 '$$rationalp   1 'rationalp-atom-rewriter)
  (declare-relation-rewriter1 '$$integerp    1 'integerp-atom-rewriter)
  (declare-relation-rewriter1 '$$naturalp    1 'naturalp-atom-rewriter)
  (declare-relation-rewriter1 '$$ratiop      1 'ratiop-atom-rewriter)
  (declare-relation-rewriter1 '$$floatp      1 'floatp-atom-rewriter)
  
  (declare-relation-rewriter1 '$$less        2 'less-atom-rewriter)
  (declare-relation-rewriter1 '$$lesseq      2 'lesseq-atom-rewriter)
  (declare-relation-rewriter1 '$$greater     2 'greater-atom-rewriter)
  (declare-relation-rewriter1 '$$greatereq   2 'greatereq-atom-rewriter)
  
  ;; operations on rationals
  (declare-function '$$sum        2 :rewrite-code 'sum-term-rewriter        :sort 'rational)
  (declare-function '$$product    2 :rewrite-code 'product-term-rewriter    :sort 'rational)
  (declare-function '$$difference 2 :rewrite-code 'difference-term-rewriter :sort 'rational)
  (declare-function '$$uminus     1 :rewrite-code 'uminus-term-rewriter     :sort 'rational)
  (declare-function '$$quotient   2 :rewrite-code 'quotient-term-rewriter   :sort 'rational)
  (declare-function '$$ceiling    2 :rewrite-code 'ceiling-term-rewriter    :sort 'integer)
  (declare-function '$$floor      2 :rewrite-code 'floor-term-rewriter      :sort 'integer)
  (declare-function '$$round      2 :rewrite-code 'round-term-rewriter      :sort 'integer)
  (declare-function '$$truncate   2 :rewrite-code 'truncate-term-rewriter   :sort 'integer)
  (let-options ((print-symbol-table-warnings nil))
    (declare-function '$$ceiling  1 :rewrite-code 'ceiling-term-rewriter    :sort 'integer)
    (declare-function '$$floor    1 :rewrite-code 'floor-term-rewriter      :sort 'integer)
    (declare-function '$$round    1 :rewrite-code 'round-term-rewriter      :sort 'integer)
    (declare-function '$$truncate 1 :rewrite-code 'truncate-term-rewriter   :sort 'integer))
  (declare-function '$$float      1 :rewrite-code 'float-term-rewriter      :sort 'float)
  
  ;; operations on floats
  (declare-function '$$sum_float        2 :rewrite-code 'sum_float-term-rewriter        :sort 'float)
  (declare-function '$$product_float    2 :rewrite-code 'product_float-term-rewriter    :sort 'float)
  (declare-function '$$difference_float 2 :rewrite-code 'difference_float-term-rewriter :sort 'float)
  (declare-function '$$uminus_float     1 :rewrite-code 'uminus_float-term-rewriter     :sort 'float)
  (declare-function '$$quotient_float   2 :rewrite-code 'quotient_float-term-rewriter   :sort 'float)
  (declare-function '$$ceiling_float    2 :rewrite-code 'ceiling_float-term-rewriter    :sort 'float)
  (declare-function '$$floor_float      2 :rewrite-code 'floor_float-term-rewriter      :sort 'float)
  (declare-function '$$round_float      2 :rewrite-code 'round_float-term-rewriter      :sort 'float)
  (declare-function '$$truncate_float   2 :rewrite-code 'truncate_float-term-rewriter   :sort 'float)
  (let-options ((print-symbol-table-warnings nil))
    (declare-function '$$ceiling_float  1 :rewrite-code 'ceiling_float-term-rewriter    :sort 'float)
    (declare-function '$$floor_float    1 :rewrite-code 'floor_float-term-rewriter      :sort 'float)
    (declare-function '$$round_float    1 :rewrite-code 'round_float-term-rewriter      :sort 'float)
    (declare-function '$$truncate_float 1 :rewrite-code 'truncate_float-term-rewriter   :sort 'float))
  (declare-function '$$rationalize      1 :rewrite-code 'rationalize-term-rewriter      :sort 'rational)
  
  ;; operations on integers
  (declare-function '$$sum_integer        2 :rewrite-code 'sum_integer-term-rewriter        :sort 'integer)
  (declare-function '$$product_integer    2 :rewrite-code 'product_integer-term-rewriter    :sort 'integer)
  (declare-function '$$difference_integer 2 :rewrite-code 'difference_integer-term-rewriter :sort 'integer)
  (declare-function '$$uminus_integer     1 :rewrite-code 'uminus_integer-term-rewriter     :sort 'integer)
  (declare-function '$$quotient_integer   2 :rewrite-code 'quotient_integer-term-rewriter   :sort 'integer)
  (declare-function '$$ceiling_integer    2 :rewrite-code 'ceiling_integer-term-rewriter    :sort 'integer)
  (declare-function '$$floor_integer      2 :rewrite-code 'floor_integer-term-rewriter      :sort 'integer)
  (declare-function '$$round_integer      2 :rewrite-code 'round_integer-term-rewriter      :sort 'integer)
  (declare-function '$$truncate_integer   2 :rewrite-code 'truncate_integer-term-rewriter   :sort 'integer)
  )

(defun numberp-atom-rewriter   (atom subst) (characteristic-atom-rewriter atom subst #'numberp   'number))
(defun realp-atom-rewriter     (atom subst) (characteristic-atom-rewriter atom subst #'realp     'real))
(defun rationalp-atom-rewriter (atom subst) (characteristic-atom-rewriter atom subst #'rationalp 'rational))
(defun integerp-atom-rewriter  (atom subst) (characteristic-atom-rewriter atom subst #'integerp  'integer))
(defun naturalp-atom-rewriter  (atom subst) (characteristic-atom-rewriter atom subst #'naturalp  'natural))
(defun ratiop-atom-rewriter    (atom subst) (characteristic-atom-rewriter atom subst #'ratiop    'ratio))
(defun floatp-atom-rewriter    (atom subst) (characteristic-atom-rewriter atom subst #'floatp    'float))

(defun less-atom-rewriter      (atom subst) (numeric-atom-rewriter1 atom subst #'<))
(defun lesseq-atom-rewriter    (atom subst) (numeric-atom-rewriter1 atom subst #'<=))
(defun greater-atom-rewriter   (atom subst) (numeric-atom-rewriter1 atom subst #'>))
(defun greatereq-atom-rewriter (atom subst) (numeric-atom-rewriter1 atom subst #'>=))

(defun sum-term-rewriter        (term subst) (numeric-term-rewriter1 term subst #'rationalp #'+))
(defun product-term-rewriter    (term subst) (numeric-term-rewriter1 term subst #'rationalp #'*))
(defun difference-term-rewriter (term subst) (numeric-term-rewriter1 term subst #'rationalp #'-))
(defun uminus-term-rewriter     (term subst) (numeric-term-rewriter1 term subst #'rationalp #'-))
(defun quotient-term-rewriter   (term subst) (numeric-term-rewriter2 term subst #'rationalp #'/))
(defun ceiling-term-rewriter    (term subst) (numeric-term-rewriter2 term subst #'rationalp #'ceiling))
(defun floor-term-rewriter      (term subst) (numeric-term-rewriter2 term subst #'rationalp #'floor))
(defun round-term-rewriter      (term subst) (numeric-term-rewriter2 term subst #'rationalp #'round))
(defun truncate-term-rewriter   (term subst) (numeric-term-rewriter2 term subst #'rationalp #'truncate))
(defun float-term-rewriter      (term subst) (numeric-term-rewriter1 term subst #'rationalp #'float))

(defun sum_float-term-rewriter        (term subst) (numeric-term-rewriter1 term subst #'floatp #'+))
(defun product_float-term-rewriter    (term subst) (numeric-term-rewriter1 term subst #'floatp #'*))
(defun difference_float-term-rewriter (term subst) (numeric-term-rewriter1 term subst #'floatp #'-))
(defun uminus_float-term-rewriter     (term subst) (numeric-term-rewriter1 term subst #'floatp #'-))
(defun quotient_float-term-rewriter   (term subst) (numeric-term-rewriter2 term subst #'floatp #'/))
(defun ceiling_float-term-rewriter    (term subst) (numeric-term-rewriter2 term subst #'floatp #'fceiling))
(defun floor_float-term-rewriter      (term subst) (numeric-term-rewriter2 term subst #'floatp #'ffloor))
(defun round_float-term-rewriter      (term subst) (numeric-term-rewriter2 term subst #'floatp #'fround))
(defun truncate_float-term-rewriter   (term subst) (numeric-term-rewriter2 term subst #'floatp #'ftruncate))
(defun rationalize-term-rewriter      (term subst) (numeric-term-rewriter1 term subst #'floatp #'rationalize))

(defun sum_integer-term-rewriter        (term subst) (numeric-term-rewriter1 term subst #'integerp #'+))
(defun product_integer-term-rewriter    (term subst) (numeric-term-rewriter1 term subst #'integerp #'*))
(defun difference_integer-term-rewriter (term subst) (numeric-term-rewriter1 term subst #'integerp #'-))
(defun uminus_integer-term-rewriter     (term subst) (numeric-term-rewriter1 term subst #'integerp #'-))
(defun quotient_integer-term-rewriter   (term subst) (numeric-term-rewriter1 term subst #'integerp (integer-quotient-rounding-mode?)))                                                                                                   
(defun ceiling_integer-term-rewriter    (term subst) (numeric-term-rewriter2 term subst #'integerp #'ceiling))
(defun floor_integer-term-rewriter      (term subst) (numeric-term-rewriter2 term subst #'integerp #'floor))
(defun round_integer-term-rewriter      (term subst) (numeric-term-rewriter2 term subst #'integerp #'round))
(defun truncate_integer-term-rewriter   (term subst) (numeric-term-rewriter2 term subst #'integerp #'truncate))

(defun numeric-atom-rewriter1 (atom subst fun)
  (let ((args nil))
    (dolist (arg (args atom) (if (apply fun (nreverse args)) true false))
      (if (dereference arg subst :if-constant (numberp arg))
          (if (implies args (iff (floatp (first args)) (floatp arg)))
              (push arg args)
              (return none))
          (return none)))))

(defun numeric-term-rewriter1 (term subst pred fun)
  ;; if all arguments satisfy pred return result of apply fun to them
  (let ((args nil))
    (dolist (arg (args term) (declare-constant (apply fun (nreverse args))))
      (if (dereference arg subst :if-constant (funcall pred arg))
          (push arg args)
          (return none)))))

(defun numeric-term-rewriter2 (term subst pred fun)
  ;; like numeric-term-rewriter1 but last argument must be nonzero if there is more than one argument
  (let ((args nil))
    (dolist (arg (args term) (if (and (rest args) (zerop (first args))) none (declare-constant (apply fun (nreverse args)))))
      (if (dereference arg subst :if-constant (funcall pred arg))
          (push arg args)
          (return none)))))

;;; code-for-numbers2.lisp EOF
